ds:x:Id fp Type, da:k:Knd fp Type, l:IdLnk, tgs:Id List, ks:Knd List,
g:(k:{k:Knd| (k  ks) }(tg:{tg:Id| (tg  tgs) }
g:(k:{k:Knd| (k  ks) }((State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List).
no_repeats(Id;tgs)
 (tgtgs. rcv(l,tg)  dom(da))
 (es:ES.
 ((kks. sends k(v:da(k)?Void) on l:tagged(g(k),State(ds),v):dt(l;da))
 (& (tgtgs. only events in ks send on l with tg)
 ( es-decls(es;source(l);ds;da)
 ( with decls ds 
 ( with decls da
 ( sends on l from e 
 ( include if deq-member(KindDeq;kind(e);ks)
 ( include if tagged-list-messages((state when e);val(e);g(kind(e)))
 ( include else nil fi 
 ( and only these for tags in tgs) 

latex

Definitions

x:A. B(x), P  Q, t  T, Prop, x. t(x), with decls ds dasends on l from e include f(e) and only these for tags in tgs, P & Q, A & B, x:A. B(x), T, True, P  Q, P  Q, S  T, Top, 1of(t), f o g, State(ds), sends-msgs(s;v;tg_f), state@i, Valtype(da;k), P  Q, f(x)?z, {T}, if b t else f fi, true, false, e@i. P(e), ||as||, Y, SQType(T), AB, A, False, (x  l), {i..j}, i  j < k, xL. P(x), S  T, x(s), only events in L send on l with tg, sends k(v:T) on l:tagged(g,State(ds),v):dt, rcvs from e on l = L, SqStable(P), Knd, , Unit, , Id, tagged-list-messages(s;v;L), 2of(t),

Lemmas

event system wf, l all wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, rcv wf, no repeats wf, l member wf, decl-state wf, ma-valtype wf, fpf-cap wf, Id wf, IdLnk wf, fpf wf, Knd wf, es-decls wf, lsrc wf, es-decls-iff, es-E wf, es-isrcv wf, es-lnk wf, es-tag wf, es-sender wf, es-rcv-kind, squash wf, true wf, es-kind wf, es-loc wf, ldst wf, es-loc-sender, id-deq wf, es-dt wf, top wf, map-map, subtype rel list, implies functionality wrt iff, map wf, member map, l member set, list-set-type-property, decidable assert, sq stable from decidable, pi1 wf, concat wf, subtype rel self, deq wf, es-state-when wf, subtype rel dep function, es-vartype wf, list-set-type-member, decidable l member, decidable equal Id, subtype rel transitivity, es-valtype wf, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, Knd sq, deq-member wf, assert-deq-member, not functionality wrt iff, int seg wf, es-val wf, length wf1, tagged-list-messages wf, length-map, es-rcv-from-implies, es-index wf, es-Msgl wf, es-sends wf, select wf, map select, le wf, member-concat, es-dt-cap, pi2 wf, Id sq, es-rcv-from-member-index, es-dt-dom, sends-p wf, fpf-cap-void-subtype